M1, M2:MsgA.
M1  M2
 (a:Id, s:M2.state. a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s)) 

latex

Definitions	f(x)?z, KindDeq, locl(a), Top, unsolvable M.pre(a,s), M.da(a), a declared in M, M.state, M1  M2, MsgA, Valtype(da;k), z != f(x)  P(a;z), IdDeq, IdLnk, f  g, A & B, if b t else f fi, Unit, P  Q, P & Q, x  dom(f), a:A fp B(a), x. t(x), , b, b, False, P  Q, f(x), Prop, Knd, State(ds), Id, A, x:A. B(x), t  T
Lemmas	not wf, assert wf, bnot wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool wf, Knd wf, locl wf, Kind-deq wf, top wf, fpf-cap wf, ma-state wf, Id wf, fpf-ap wf, id-deq wf, ma-decla wf, ma-st wf, ma-sub wf, msga wf